A:Type, r:(AA), L:A List.
(a:A. r(a,a))
 null(L)
 (L1, L2:A List.
 (L = (L1 @ L2) & null(L2) & (bL2. r(b,last(L))) & (null(L1)  r(last(L1),last(L)))) 

latex

Definitions	t  T, x:A. B(x), , True, False, P  Q, A, x(s1,s2), b, xL. P(x), P & Q, x:A. B(x), null(as), P  Q, Dec(P), last(L), Prop, x. t(x), as @ bs, reduce(f;k;as), P  Q, P  Q, hd(l), i<j, ij, l[i], if b t else f fi, ||as||, ij, AB, , {T}, SQType(T), {a:T}
Lemmas	uni sat imp in uni set, iff imp equal bool, minus mono wrt eq, singleton properties, singleton wf, last cons, le wf, cons one one, nat wf, non neg length, length wf1, member wf, l all cons, assert of null, false wf, l all reduce, l all nil, null wf2, append wf, l all wf, last wf, decidable assert, null wf, not wf, true wf, assert wf, bool wf